(set-logic QF_BV)
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
(declare-fun z () (_ BitVec 32))
(declare-fun w () (_ BitVec 32))
(assert 
  (let ((e5 (bvshl z y))) 
  (let ((e6 (bvsub e5 w))) 
  (let ((e7 (bvshl e6 x))) 
  (let ((e14 (= e7 e5))) 
  (let ((e22 (xor true e14))) 
  (let ((e24 (xor e22 true))) 
  (let ((e25 e24)) 
  (let ((e28 (xor e25 true))) e28)))))))))
(check-sat)
